$\forall$${\it Pgm}$, ${\it Sem}$:Type, ${\it equiv}$:(${\it Sem}$$\rightarrow$${\it Sem}$$\rightarrow$Prop), $S$:(${\it Pgm}$$\rightarrow$${\it Sem}$), $X$:(${\it Sem}$$\rightarrow$Prop), ${\it kpr}$:(${\it Sem}$$\rightarrow$${\it Pgm}$).
\\[0ex]${\it kpr}$ $\vDash$ $X$ $\in$ Prop